#include "rewrite.h"
#include "info/icut.h"
#include "rwtdb.h"

// TODO 
// 1. if backward validation is not needed
// 2. rwtdb could be merge to here 

extern unsigned short belookup[4][256][4];
inline unsigned short be( unsigned short s, unsigned short in , unsigned short c){
   return belookup[s][in][c];
}
static unsigned short special_fun[(1<<(1<<DBSIZE))] = {};
static unsigned short binv( unsigned short f , unsigned short i )
{
   switch( i )
   {
      case 0 : return ((f&0x00FF)<<8) | ((f&0xFF00)>>8);
      case 1 : return ((f&0x0F0F)<<4) | ((f&0xF0F0)>>4);
      case 2 : return ((f&0x3333)<<2) | ((f&0xCCCC)>>2);
      case 3 : return ((f&0x5555)<<1) | ((f&0xAAAA)>>1);
   }
   assert(false);
   return 0;
}
static void static_init()
{
   special_fun[ 0xFF00] = special_fun[ 0x00FF] = 1;
   special_fun[ 0xF0F0] = special_fun[ 0x0F0F] = 2;
   special_fun[ 0x3333] = special_fun[ 0xCCCC] = 3;
   special_fun[ 0x5555] = special_fun[ 0xAAAA] = 4;
   special_fun[ 0x0000] = special_fun[ 0xFFFF] = 5;   
}
bool InfoCut::exist( Cut & c )
{
   for( int i = 0 ; i < DBSIZE ; ++ i )
      if( _focnt[ c[i] ] == 0 )
      {
         unsigned eqn = eqIdx( c[i] );
         if( _focnt[eqn] != 0 )
         {
            if( ph(eqn) ^ ph( c[i] ) ) 
               c.fun = binv( c.fun , i );
            c[i] = eqn;
         }else
            return false;
      }
   return true;
}
inline void expand( Cut & c )
{
   c.node[3] = 0;
   c.fun = be( 3 , c.fun , 3 );
}
void Rewrite::run( unsigned idx )
{
   unsigned outcnt = 0 ;
   std::swap( outcnt , _cut._focnt[idx] );

   short    gain = 0 , cost , pay ;
   unsigned winner = idx;

   if(!_cut.setted(idx))_cut.update(idx);

   //for( unsigned innum = 3 ; innum > 1 ; -- innum )
   const unsigned innum = 3;
   {
      Cut * v = _cut._cut[idx][innum].dat;
      int s = _cut._cut[idx][innum].size;
      for( int i = 0 ; i < s ; ++ i )
      {
         Cut c = v[i];
   //      if( innum == 2 ) expand(c);
         if( _cut.exist( c ) == false || _db->setted(c.fun) == false )continue;
   
         mark_t * mrk  = _cut._mrk.data;
   
         mrk[ c[0] ] = mrk[ c[1] ] = mrk[ c[2] ] = mrk[ c[3] ] = true;
         cost = _cut.get_cone( idx , _tmp_cone);
         mrk[ c[0] ] = mrk[ c[1] ] = mrk[ c[2] ] = mrk[ c[3] ] = false;
   
         if( cost <= gain ){ _cut.resume( _tmp_cone.data , _tmp_cone.sz) ; continue;}
         
         pay=special_fun[c.fun];// reuse pay variable 
         if( pay ) { gain=cost;_cut.resume( _tmp_cone.data , _tmp_cone.sz);winner=((pay==5)?0:c[pay-1]);continue;}
   
         int plus = (REPLACEMENT==2)?((winner==idx)):REPLACEMENT; // parameter constrol 
         pay = _db->construct( c.fun , c , DBSIZE , cost-gain+plus , winner );
         if( cost - pay > gain) { gain=cost-pay;}
   
         _cut.resume( _tmp_cone.data , _tmp_cone.sz);
      }
   }
   if( _cut.accept( idx , winner ) )
   {
      _cut._cut.growTo( _cut.size() );
      _cut.replace( idx , winner , outcnt );
   }
   else _cut._focnt[ idx ] = outcnt;
}
void Rewrite::run()
{
   init();

   int s , d , inc ; 
   if( DIRECTION == 0 ) s = _cut._andFlag , d = _cut.size() , inc = 1 ;
   else                 s = _cut.size()-1 , d = _cut._andFlag -1 , inc = -1;
   
   for( int i = s ; i != d ; i +=inc )
      if( _cut._focnt[i] != 0 ) 
         run(i);
}

Rewrite::Rewrite( InfoCut & c )
   :_cut(c) 
{
   static_init();

   DIRECTION   = 0;
   REPLACEMENT = 0;
}
void Rewrite::init()
{
   _cut.validation();
   _cut.create_base();
   if( DIRECTION == (unsigned short)1 )
      for( unsigned i = _cut._andFlag ; i < _cut.size() ; ++i )
         _cut.update(i);
}
void Rewrite::read_db( RewriteDB & db )
{
   _db = & db;
   _db->_ckt =  const_cast< StrashAIG * >( dynamic_cast<const StrashAIG *>(& _cut ) );
   _db->_focnt = & _cut._focnt;
   _db->_info  = & _cut;
}
